A:Type, f:(A(A + top)). SWellFounded(p-graph(A; f)(y,x))  (x:A. final-iterate(f; x)  A) 

latex

Definitions	#$n, t  T, n - m, x:A. B(x), {x:A| B(x)} , , x:AB(x), P  Q, final-iterate(f; x), b, A c B, False, A, A  B, b, s = t, prop{i:l}, , void, isect(A; x.B(x)), top, subtype(S; T), left + right, suptype(S; T), can-apply(f; x), x:A  B(x), P  Q, P  Q, Unit, x:A. B(x), SWellFounded(R(x;y)), Type, x,y. t(x;y), p-graph(A; f), ge(i; j), -n, n + m, f(a), do-apply(f; x), a < b
Lemmas	ge wf, nat properties, strongwellfounded wf, nat wf, le wf, eqtt to assert, iff transitivity, eqff to assert, assert of bnot, can-apply wf, top wf, bool wf, bnot wf, not wf, assert wf, do-apply wf